<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Issue2401</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">% The example below is, modulo a small change, due to Andrés
% Sicard-Ramírez.

\documentclass{article}

\usepackage{agda}

\begin{document}

av
</a><a id="146" class="Markup">\begin{code}</a>
  <a id="161" class="Keyword">module</a> <a id="168" href="Issue2401.html" class="Module">Issue2401</a> <a id="178" class="Keyword">where</a>

    <a id="189" class="Keyword">data</a> <a id="Bool"></a><a id="194" href="Issue2401.html#194" class="Datatype">Bool</a> <a id="199" class="Symbol">:</a> <a id="201" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="205" class="Keyword">where</a>
      <a id="Bool.true"></a><a id="217" href="Issue2401.html#217" class="InductiveConstructor">true</a>  <a id="223" class="Symbol">:</a> <a id="225" href="Issue2401.html#194" class="Datatype">Bool</a>
      <a id="Bool.false"></a><a id="236" href="Issue2401.html#236" class="InductiveConstructor">false</a> <a id="242" class="Symbol">:</a> <a id="244" href="Issue2401.html#194" class="Datatype">Bool</a>
      <a id="Bool.dunno"></a><a id="255" href="Issue2401.html#255" class="InductiveConstructor">dunno</a> <a id="261" class="Symbol">:</a> <a id="263" href="Issue2401.html#194" class="Datatype">Bool</a>
      <a id="Bool.aa"></a><a id="274" href="Issue2401.html#274" class="InductiveConstructor">aa</a>    <a id="280" class="Symbol">:</a> <a id="282" class="Comment">{- \end{code} -}</a> <a id="299" href="Issue2401.html#194" class="Datatype">Bool</a>

<a id="305" class="Markup">\end{code}</a><a id="315" class="Background">
bleh

\end{document}</a></pre></body></html>